T:Type, P:(Tprop{i:l}), L1,L2:(T List).
l_all(append(L1; L2); T; x.P(x))  (l_all(L1; T; x.P(x))  l_all(L2; T; x.P(x))) 

latex

Definitions	guard(T), True, P  Q, t  T, P  Q, P  Q, P  Q, x(s), l_all(L; T; x.P(x)), P  Q, prop{i:l}, x:A. B(x)
Lemmas	append wf, l member wf, member append